$\forall$$M$, $A$:MsgA, $k$:Knd, $y$:Id, $f$:($A$.state$\rightarrow$$A$.da($k$)$\rightarrow$ds($A$)($y$)?Void).
\\[0ex]$M$.rframe($A$.effect $f$ of $k$ on $y$) $\in$ Prop